\begin{tabbing}
chain{-}replication{-}acks\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Rsp}$; ${\it isupdate}$; ${\it In}$; ${\it Out}$; ${\it Sys}$; ${\it Ack}$; $f$; $g$; ${\it Delta}$; $Q$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=fifo{-}antecedent(${\it es}$;${\it Sys}$;$f$) \& fifo{-}antecedent(${\it es}$;${\it Ack}$;$g$)\+
\\[0ex]\& ($\forall$$u$:E(${\it Sys}$). ($f$($u$) = $u$) $\Leftarrow\!\Rightarrow$ ($\uparrow$($u$ $\in_{b}$ ${\it In}$)))
\\[0ex]\& (E(${\it In}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]\& (E(${\it Out}$) $\subseteq$r E(${\it Sys}$))
\\[0ex]\& (E(${\it Out}$) $\subseteq$r E(${\it Ack}$))
\\[0ex]\& ($\forall$$e$:E(${\it In}$). ($\neg$($\uparrow$(${\it isupdate}$(${\it In}$($e$))))) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]\& ($\forall$$e$:E(${\it Sys}$). ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it In}$))) $\Rightarrow$ (loc($f$($e$)) = loc($e$)) $\Rightarrow$ ($\neg$($\uparrow$($e$ $\in_{b}$ ${\it Out}$))))
\\[0ex]\& input{-}forwarding\=\{i:l\}\+
\\[0ex](${\it es}$; ${\it Cmd}$; ${\it Sys}$; ${\it isupdate}$; ${\it In}$; $f$)
\-\\[0ex]\& ($\exists$\=${\it chain}$:\{$e$:E$\mid$ ($\uparrow$($e$ $\in_{b}$ ${\it Sys}$)) $\vee$ ($\uparrow$($e$ $\in_{b}$ ${\it Ack}$))\} $\rightarrow$(Id List)\+
\\[0ex](chain{-}config(${\it es}$;p{-}conditional(${\it Ack}$; ${\it Sys}$);${\it chain}$)
\\[0ex]\& chain{-}consistent($f$;${\it chain}$)
\\[0ex]\& (\=$\forall$$e$:E(${\it Ack}$).\+
\\[0ex]($\neg$(loc($g$($e$)) = loc($e$)))
\\[0ex]$\Rightarrow$ \=(adjacent(Id;${\it chain}$($e$);loc($e$);loc($g$($e$)))\+
\\[0ex]\& adjacent(Id;${\it chain}$($g$($e$));loc($e$);loc($g$($e$)))))))
\-\-\-\\[0ex]\& ($\forall$$e$:E(${\it Ack}$). (loc($g$($e$)) = loc($e$)) $\Rightarrow$ ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)))
\\[0ex]\& ($\forall$$e$:E(${\it Ack}$). ($\uparrow$($e$ $\in_{b}$ ${\it Out}$)) $\Rightarrow$ ($g$($e$) = $e$))
\\[0ex]\& ($\forall$$e$:E(${\it Ack}$). ($\uparrow$(($g$($e$)) $\in_{b}$ ${\it Out}$)) $\Rightarrow$ is{-}query(${\it In}$;${\it isupdate}$;$g$($e$)) $\Rightarrow$ ($g$($e$) = $e$))
\\[0ex]\& (\=$\forall$$e$:E(${\it Out}$).\+
\\[0ex](\=is{-}query(${\it In}$;${\it isupdate}$;$e$)\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = $Q$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$)),${\it In}$($e$))))
\-\\[0ex]\& (\=($\neg$is{-}query(${\it In}$;${\it isupdate}$;$e$))\+
\\[0ex]$\Rightarrow$ (${\it Out}$($e$) = ${\it Delta}$(filter(${\it isupdate}$;es{-}interface{-}history(${\it es}$; ${\it Sys}$; $e$))))))
\-\-\\[0ex]\& (\=$\forall$$e$:E(${\it Ack}$).\+
\\[0ex]${\it Ack}$($e$) = if $e$ $\in_{b}$ ${\it Out}$ then $\parallel$filter(${\it isupdate}$;${\it Sys}$($e$))$\parallel$ else ${\it Ack}$($g$($e$)) fi )
\-\-
\end{tabbing}